Verification of an integrated circuit design typically involves testing the circuit design before the design is physically implemented as a circuit on a chip, so that bugs in the circuit design can be identified before the expense of fabrication occurs. Conventional verification methods generally use software simulation tools to verify design models at different levels of description of the circuit design such as an RTL (Register Transfer Logic) description of the circuit design, a layout of the circuit design, etc.
Because most of the system-on-chip designs include relatively large, fast and complex integrated memories, on-chip buses, and sophisticated modules or cores, simulation of descriptions of a circuit design has become increasingly time consuming, complex and difficult. Furthermore, simulation of high levels of abstraction of a circuit design cannot guarantee accuracy with regard to a physical circuit fabricated on the chip according to the corresponding high level models.
Verifying the actual hardware circuit and debugging the hardware circuit (also called silicon debug) are difficult and costly problems that delay volume production and market entry. The major reason for these difficulties resides in the lack of control and visibility over critical signals.
In the prior art, an important tool for verification of integrated circuits is referred to as “Model Checking”. Model Checking is a formal verification technique introduced around 1981 in various theoretical works: E. M. Clarke and E. A. Emerson “Design and synthesis of synchronization skeletons using branching time temporal logic.” In Logic of Programs: Workshop, Yorktown Heights N.Y. LNCS 131 Springer Verlag May 1981; J.-P. Queille and J. Sifakis “Specification and Verification of Concurrent Systems in Cesar.” Int. Symp. On Programming LNCS 132 Springer Verlag 1982. However, it was industrialized and used for hardware verification only in the late 90's http://www.eet.com/news/98/1024news/blda.html.
Basically, a Model Checker is a software tool which explores states reachable from an initial state of a transition system, to check whether an “assertion” is verified, or proven, for all reachable states, or whether the assertion fails for some states. In the latter case, the tool is able to define and exhibit a “trace”, i.e. a sequence of reachable states starting from the initial state to a failure (state where the assertion fails).
When applied to integrated circuit design, a Model Checker reads in:                a design description for an integrated circuit, which contains state elements, primary inputs (PIs), and primary outputs (POs),        a set of constraints C (optional),        an initial state I,        at least one assertion to be proven over the entire reachable state space.        
A state s is defined as a Boolean function over all state elements, (including PIs, and POs) of the design. A state s is reachable from state I if and only if there exists a sequence of “transitions” which goes from I to s with respect to the set of constraints C, where a transition is defined as the functioning of the design for one cycle. A “deep” trace extends over a relatively long sequence of transitions with a large number of different states (no regular repetition of transitions).
In operation, a Model Checker starts compiling a design description, constraints and one or more assertions, into a basic logic format, which is used to compute states and evaluate assertions. After the basic logic is determined, the Model Checker progresses in its exploration of the entire reachable state space starting from the initial state. At each current state, it:                computes all possible next states from a current state respecting the constraints C,        compares all new states to the already reached states to decide if it has already been explored or not; marks all new states accordingly, as explored or not.        evaluates the assertion to be proven as true or false in any new state,        marks the current state as “explored” and picks a new current state among the reached and unexplored states, and        stops when all states have been explored, or after predetermined processing time limit has been reached.        
Due to the complexity of integrated circuits, in practice, a Model Checker often does not finish its exploration (over all possible states) because it has to consider too many states (known as “state explosion” in the literature); instead, a limited subset of the reachable state space is explored, limited by the processing time limit.
Conventional formal verification tools operate on a description of a circuit design and do not directly operate on a fabricated circuit on a chip. There is a need for a new apparatus and method for analyzing and debugging integrated circuits, which uses control and visibility provided by tools like a Model Checker, together with speed and accuracy which can be provided by processing on an actual chip.